ds:fpf(Id; x.Type), a,b:fpf((:Knd  Id); kz.top).
update-spec-decl(a; ds)
 update-spec-decl(b; ds)
 update-spec-decl(update-spec-join(a; b); ds) 

latex

Definitions	Id, t  T, Type, x. t(x), x:A. B(x), fpf(A; a.B(a)), Knd, x:A  B(x), top, x.A(x), x:AB(x), type List, update-spec-vars(upd), id-deq, fpf-dom(eq; x; f), b, prop{i:l}, (x  l), P  Q, update-spec-join(a; b), update-spec-decl(upd; ds), left + right, P  Q, P  Q, P  Q, Kind-deq, product-deq(A; B; a; b), fpf-join(eq; f; g), fpf-domain(f), t.2, map(f; as)
Lemmas	map wf, pi2 wf, fpf-domain wf, fpf-join wf, product-deq wf, Kind-deq wf, update-spec-join-vars, l member wf, assert wf, fpf-dom wf, id-deq wf, fpf-trivial-subtype-top, top wf, Knd wf, fpf wf, Id wf